$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$), $e$:E. es{-}prior{-}interface{-}vals(${\it es}$;$X$;$e$) $\in$ ($A$ List)